proposition: Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c.
proof: Proof. induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2). - apply Q2R_0. - apply Q2R_1. - reflexivity. - unfold Q2R. simpl. rewrite Rinv_1. reflexivity. - apply Q2R_plus. - apply Q2R_minus. - apply Q2R_mult. - destruct z. 1:destruct (CPowR0 z c) eqn:C; unfold CPowR0 in C. + rewrite andb_true_iff in C. destruct C as (C1 & C2). rewrite Z.ltb_lt in C1. apply Qeq_bool_eq in C2. rewrite C2. simpl. assert (z <> 0%Z). { intro ; subst. apply Z.lt_irrefl in C1. auto. } rewrite Qpower0 by auto. apply Q2R_0. + rewrite Q2RpowerRZ. * rewrite IHc. reflexivity. * rewrite andb_false_iff in C. destruct C. -- simpl. apply Z.ltb_ge in H. right. Ztac.normZ. Ztac.slia H H0. -- left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. destruct Qpower_theory. rewrite <- nat_N_Z. rewrite rpow_pow_N. destruct R_power_theory. rewrite <- (Nnat.Nat2N.id n) at 2. rewrite rpow_pow_N0. apply Q2R_pow_N. - rewrite <- IHc. unfold CInvR0. apply Q2R_inv_ext. - rewrite <- IHc. apply Q2R_opp. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant