proposition: Lemma inj_Q_div : forall q1 q2 H, inj_Q (q1/q2)%Q [=] (inj_Q q1[/]inj_Q q2[//]H).
proof: Proof. intros. apply mult_cancel_rht with (inj_Q q2);[apply H|]. apply eq_symmetric. eapply eq_transitive;[|apply inj_Q_mult]. eapply eq_transitive;[apply div_1|]. apply inj_Q_wd. simpl. field. apply inj_Q_strext. stepr ([0]:R1). apply H. rstepl (inj_Q q1[-]inj_Q q1). apply eq_symmetric. eapply eq_transitive;[|apply inj_Q_minus]. apply inj_Q_wd. unfold cg_minus. simpl. ring. Qed.
imports: CoRN.model.reals.Cauchy_IR CoRN.model.monoids.Nmonoid CoRN.model.rings.Zring CoRN.algebra.CRing_Homomorphisms CoRN.algebra.Expon Coq.QArith.Qpower CoRN.tactics.CornTac