proposition: Lemma inj_Q_wd : forall q1 q2, (q1 [=] q2) -> inj_Q q1 [=] inj_Q q2.
proof: Proof. intros. apply not_ap_imp_eq. intro. cut (~ (q1 [=] q2)). intro H1. apply H1. assumption. change (q1[~=]q2) in |- *. apply ap_imp_neq. apply inj_Q_strext. assumption. 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