proposition: Lemma zring_strext : forall m n : Z_as_CRing, (zring (R:=R1) m [#] zring n) -> m [#] n.
proof: Proof. intros m n. case m. case n. intro H. exfalso. cut ([0] [=] ([0]:R1)). change (~ ([0] [=] ([0]:R1))) in |- *. apply ap_imp_neq. simpl in H. assumption. apply eq_reflexive_unfolded. intros. simpl in |- *. red in |- *. discriminate. intros. simpl in |- *. red in |- *. discriminate. case n. intros. simpl in |- *. red in |- *. discriminate. intros. simpl in |- *. intro. cut (Not (zring (R:=R1) (BinInt.Zpos p0) [#] zring (R:=R1) (BinInt.Zpos p))). intro H1. elim H1. assumption. apply eq_imp_not_ap. rewrite H. apply eq_reflexive_unfolded. intros. simpl in |- *. red in |- *. discriminate. case n. intros. simpl in |- *. red in |- *. discriminate. intros. simpl in |- *. red in |- *. discriminate. intros. simpl in |- *. intro. cut (Not (zring (R:=R1) (Zneg p0) [#] zring (R:=R1) (Zneg p))). intro H1. elim H1. assumption. apply eq_imp_not_ap. rewrite H. apply eq_reflexive_unfolded. 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