proposition: Lemma R_mult_ap_zero' : forall x y, R_mult x y [#] [0] -> x [#] [0].
proof: Proof. intros x y Hxy. elim (CS_seq_bounded _ (CS_seq _ y) (CS_proof _ y)); intros K HK Hy; elim Hy; clear Hy; intros Ny HNY. set (z := Build_CauchySeq _ _ (CS_seq_mult _ _ _ (CS_seq_const _ (Two[*]K)) (CS_proof _ x)) :R_CAbGroup) in *. elim (ap_cotransitive_unfolded _ _ _ Hxy z); intro Hap; elim Hap; intro Hlt; elim Hlt; intros N HN; elim HN; clear Hap Hlt HN; intros e He HN. right. cut (forall n : nat, Ny <= n -> [0] [<] Two[*]K[-]CS_seq _ y n); [ intro Hy' | intros n Hn ]. set (KK := e[/] _[//]mult_resp_ap_zero _ _ _ (three_ap_zero _) (pos_ap_zero _ _ HK)) in *. exists (Nat.max N Ny); exists KK. unfold KK in |- *; apply div_resp_pos; auto. apply mult_resp_pos; auto; apply pos_three. intros; simpl in |- *; unfold KK in |- *. cut (N <= n); [ intro Hn | apply Nat.le_trans with (Nat.max N Ny); auto with arith ]. cut (Ny <= n); [ intro Hn' | apply Nat.le_trans with (Nat.max N Ny); auto with arith ]. apply leEq_transitive with (e[/] _[//]pos_ap_zero _ _ (Hy' n Hn')). apply mult_cancel_leEq with ([1][/] _[//]pos_ap_zero _ _ He). apply recip_resp_pos; auto. rstepl ([1][/] _[//]mult_resp_ap_zero _ _ _ (three_ap_zero _) (pos_ap_zero _ _ HK)). rstepr ([1][/] _[//]pos_ap_zero _ _ (Hy' n Hn')). apply recip_resp_leEq; auto. unfold cg_minus in |- *; apply shift_plus_leEq'; rstepr ([--][--]K). apply inv_resp_leEq; elim (HNY n); auto. apply shift_div_leEq; auto. eapply leEq_wdr. apply (HN n); auto. simpl in |- *; rational. apply shift_zero_less_minus; apply leEq_less_trans with K. elim (HNY n); auto. astepl ([0][+]K); astepr (K[+]K); apply plus_resp_less_rht; auto. left. cut (forall n : nat, Ny <= n -> [0] [<] Two[*]K[-]CS_seq _ y n); [ intro Hy' | intros n Hn ]. set (KK := e[/] _[//]mult_resp_ap_zero _ _ _ (three_ap_zero _) (pos_ap_zero _ _ HK)) in *. exists (Nat.max N Ny); exists KK. unfold KK in |- *; apply div_resp_pos; auto. apply mult_resp_pos; auto; apply pos_three. intros; simpl in |- *; unfold KK in |- *. cut (N <= n); [ intro Hn | apply Nat.le_trans with (Nat.max N Ny); auto with arith ]. cut (Ny <= n); [ intro Hn' | apply Nat.le_trans with (Nat.max N Ny); auto with arith ]. apply leEq_transitive with (e[/] _[//]pos_ap_zero _ _ (Hy' n Hn')). apply mult_cancel_leEq with ([1][/] _[//]pos_ap_zero _ _ He). apply recip_resp_pos; auto. rstepl ([1][/] _[//]mult_resp_ap_zero _ _ _ (three_ap_zero _) (pos_ap_zero _ _ HK)). rstepr ([1][/] _[//]pos_ap_zero _ _ (Hy' n Hn')). apply recip_resp_leEq; auto. unfold cg_minus in |- *; apply shift_plus_leEq'; rstepr ([--][--]K). apply inv_resp_leEq; elim (HNY n); auto. apply shift_div_leEq; auto. eapply leEq_wdr. apply (HN n); auto. simpl in |- *; rational. apply shift_zero_less_minus; apply leEq_less_trans with K. elim (HNY n); auto. astepl ([0][+]K); astepr (K[+]K); apply plus_resp_less_rht; auto. left. set (KK := e[/] _[//]mult_resp_ap_zero _ _ _ (two_ap_zero _) (pos_ap_zero _ _ HK)) in *. exists N; exists KK. unfold KK in |- *; apply div_resp_pos; auto. apply mult_resp_pos; auto; apply pos_two. intros; simpl in |- *; unfold KK in |- *. apply shift_div_leEq. apply mult_resp_pos; auto; apply pos_two. eapply leEq_wdr. apply (HN n H). simpl in |- *; rational. right. set (KK := e[/] _[//]mult_resp_ap_zero _ _ _ (two_ap_zero _) (pos_ap_zero _ _ HK)) in *. exists N; exists KK. unfold KK in |- *; apply div_resp_pos; auto. apply mult_resp_pos; auto; apply pos_two. intros; simpl in |- *; unfold KK in |- *. apply shift_div_leEq. apply mult_resp_pos; auto; apply pos_two. eapply leEq_wdr. apply (HN n H). simpl in |- *; rational. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection