proposition: Lemma nring_strext : forall m n : nat_as_CMonoid, (nring (R:=R1) m [#] nring (R:=R1) n) -> m [#] n.
proof: Proof. intros m n. case m. case n. intro H. simpl in |- *. red in |- *. simpl in H. cut (Not ([0] [#] ([0]:R1))). intro. intro. elim H0. assumption. apply eq_imp_not_ap. apply eq_reflexive_unfolded. intros. simpl in |- *. red in |- *. discriminate. case n. intros. simpl in |- *. red in |- *. discriminate. intros. simpl in |- *. red in |- *. intro. cut (Not (nring (R:=R1) (S n1) [#] nring (R:=R1) (S n0))). 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