Start working on coq 8.7.2 port

coq/Infra/RealRationalProps.v

@@ -48,63 +48,51 @@ Qed.
 Lemma Q2R_max (a:Q) (b:Q) :
   Rmax (Q2R a) (Q2R b) = Q2R (Qmax a b).
 Proof.
-  apply Q.max_case_strong.
-  - intros c d eq_c_d Rmax_x.
-    rewrite Rmax_x.
-    unfold Q2R.
-    rewrite <- RMicromega.Rinv_elim.
-    setoid_rewrite Rmult_comm at 1.
-    + rewrite <- Rmult_assoc.
-      rewrite <- RMicromega.Rinv_elim.
-      rewrite <- mult_IZR.
-      rewrite eq_c_d.
-      rewrite mult_IZR.
-      rewrite Rmult_comm; auto.
-      hnf; intros.
-      pose proof (pos_INR_nat_of_P (Qden d)).
-      simpl in H.
-      rewrite H in H0.
-      lra.
-    + simpl; hnf; intros.
-      pose proof (pos_INR_nat_of_P (Qden c)).
-      rewrite H in H0; lra.
-  - intros less. apply Qle_Rle in less.
-    assert (Rmax (Q2R a) (Q2R b) = Q2R a) by (apply Rmax_left; auto).
-    rewrite H; auto.
-  - intros less. apply Qle_Rle in less.
-    assert (Rmax (Q2R a) (Q2R b) = Q2R b) by (apply Rmax_right; auto).
+  destruct (Qlt_le_dec a b).
+  -  pose proof (Qlt_Rlt _ _ q) as Rlt_H.
+     rewrite Rmax_right; try lra.
+     f_equal. unfold Qmax. unfold GenericMinMax.gmax.
+     rewrite Qlt_alt in *.
+     rewrite q; auto.
+  - pose proof (Qle_Rle _ _ q) as Rle_H.
+    hnf in Rle_H.
+    destruct Rle_H.
+    + rewrite Rmax_left; try lra.
+      apply Rlt_Qlt in H.
+      f_equal; unfold Qmax. unfold GenericMinMax.gmax.
+      rewrite Qgt_alt in *.
       rewrite H; auto.
+    + rewrite Rmax_left; try lra.
+      f_equal.
+      unfold Qmax, GenericMinMax.gmax.
+      apply eqR_Qeq in H.
+      symmetry in H.
+      rewrite Qeq_alt in H. rewrite H; auto.
 Qed.
 
 Lemma Q2R_min (a:Q) (b:Q) :
     Rmin (Q2R a) (Q2R b) = Q2R (Qmin a b).
 Proof.
-  apply Q.min_case_strong.
-  - intros c d eq_c_d Rmin_x.
-    rewrite Rmin_x.
-    unfold Q2R.
-    rewrite <- RMicromega.Rinv_elim.
-    setoid_rewrite Rmult_comm at 1.
-    + rewrite <- Rmult_assoc.
-      rewrite <- RMicromega.Rinv_elim.
-      rewrite <- mult_IZR.
-      rewrite eq_c_d.
-      rewrite mult_IZR.
-      rewrite Rmult_comm; auto.
-      hnf; intros.
-      pose proof (pos_INR_nat_of_P (Qden d)).
-      simpl in H.
-      rewrite H in H0.
-      lra.
-    + simpl; hnf; intros.
-      pose proof (pos_INR_nat_of_P (Qden c)).
-      rewrite H in H0; lra.
-  - intros less. apply Qle_Rle in less.
-    assert (Rmin (Q2R a) (Q2R b) = Q2R a) by (apply Rmin_left; auto).
-    rewrite H; auto.
-  - intros less. apply Qle_Rle in less.
-    assert (Rmin (Q2R a) (Q2R b) = Q2R b) by (apply Rmin_right; auto).
+  destruct (Qlt_le_dec a b).
+  -  pose proof (Qlt_Rlt _ _ q) as Rlt_H.
+     rewrite Rmin_left; try lra.
+     f_equal. unfold Qmin. unfold GenericMinMax.gmin.
+     rewrite Qlt_alt in *.
+     rewrite q; auto.
+  - pose proof (Qle_Rle _ _ q) as Rle_H.
+    hnf in Rle_H.
+    destruct Rle_H.
+    + rewrite Rmin_right; try lra.
+      apply Rlt_Qlt in H.
+      f_equal; unfold Qmin. unfold GenericMinMax.gmin.
+      rewrite Qgt_alt in *.
       rewrite H; auto.
+    + rewrite Rmin_left; try lra.
+      f_equal.
+      unfold Qmin, GenericMinMax.gmin.
+      apply eqR_Qeq in H.
+      symmetry in H.
+      rewrite Qeq_alt in H. rewrite H; auto.
 Qed.
 
 Lemma maxAbs_impl_RmaxAbs (ivlo:Q) (ivhi:Q):

coq/Infra/RealSimps.v

@@ -77,7 +77,7 @@ Lemma Rabs_0_impl_eq (d:R):
 Proof.
   intros abs_leq_0.
   pose proof (Rabs_pos d) as abs_geq_0.
-  pose proof (Rle_antisym (Rabs d) R0 abs_leq_0 abs_geq_0) as Rabs_eq.
+  pose proof (Rle_antisym (Rabs d) 0%R abs_leq_0 abs_geq_0) as Rabs_eq.
   rewrite <- Rabs_R0 in Rabs_eq.
   apply Rsqr_eq_asb_1 in Rabs_eq.
   rewrite Rsqr_0 in Rabs_eq.