proposition: Lemma zring_less : forall m n : Z_as_CRing, (m < n)%Z -> zring (R:=R1) m [<] zring (R:=R1) n.
proof: Proof. intros m n. case m. case n. intro. apply False_rect. generalize H. change (~ (0 < 0)%Z) in |- *. apply Z.lt_irrefl. intros. simpl in |- *. astepl (nring (R:=R1) 0). astepr (nring (R:=R1) (nat_of_P p)). apply nring_less. case (ZL4' p). intro a. intro H0. rewrite H0. apply Nat.lt_0_succ. intros. apply False_rect. generalize H. change (~ (0 < Zneg p)%Z) in |- *. apply Zlt_asym. constructor. case n. intros. apply False_rect. generalize H. change (~ (BinInt.Zpos p < 0)%Z) in |- *. apply Zlt_asym. constructor. intros p1 p2. intro. simpl in |- *. astepl (nring (R:=R1) (nat_of_P p2)). astepr (nring (R:=R1) (nat_of_P p1)). apply nring_less. apply nat_of_P_lt_Lt_compare_morphism. red in H. simpl in H. assumption. intros p1 p2. intro. apply False_rect. generalize H. change (~ (BinInt.Zpos p2 < Zneg p1)%Z) in |- *. apply Zlt_asym. constructor. case n. intros. simpl in |- *. astepl [--](nring (R:=R1) (nat_of_P p)). astepr ([0]:R1). apply inv_cancel_less. astepl ([0]:R1). astepr (nring (R:=R1) (nat_of_P p)). case (ZL4' p). intro h. intros H0. rewrite H0. apply pos_nring_S. intros p1 p2. intro. simpl in |- *. case (ZL4' p1). intro h1. case (ZL4' p2). intro h2. intros. apply less_transitive_unfolded with (y := [0]:R1). astepl [--](nring (R:=R1) (nat_of_P p2)). apply inv_cancel_less. astepl ([0]:R1). astepr (nring (R:=R1) (nat_of_P p2)). rewrite e. apply pos_nring_S. astepr (nring (R:=R1) p1). rewrite e0. apply pos_nring_S. intros p1 p2. intro. simpl in |- *. astepl [--](nring (R:=R1) (nat_of_P p2)). astepr [--](nring (R:=R1) (nat_of_P p1)). apply inv_resp_less. apply nring_less. apply nat_of_P_lt_Lt_compare_morphism. red in H. simpl in H. now rewrite ZC4. 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