proposition: Lemma R_integral_domain : forall x y : R_CRing, x [#] [0] -> y [#] [0] -> x[*]y [#] [0].
proof: Proof. intros x y Hx Hy. elim Hx; intro Hlt; elim Hlt; intros Nx HN; elim HN; clear Hx Hlt HN; intros ex Hex HNx; simpl in HNx; elim Hy; intro Hlt; elim Hlt; intros Ny HN; elim HN; clear Hy Hlt HN; intros ey Hey HNy; simpl in HNy. right. exists (Nat.max Nx Ny); exists (ex[*]ey). apply mult_resp_pos; auto. intros; simpl in |- *; rstepr ([--] (CS_seq _ x n) [*][--] (CS_seq _ y n)). apply mult_resp_leEq_both; try (apply less_leEq; assumption). astepr ([0][-]CS_seq _ x n); eauto with arith. astepr ([0][-]CS_seq _ y n); eauto with arith. left. exists (Nat.max Nx Ny); exists (ex[*]ey). apply mult_resp_pos; auto. intros; simpl in |- *; rstepr ([--] (CS_seq _ x n) [*]CS_seq _ y n). apply mult_resp_leEq_both; try (apply less_leEq; assumption). astepr ([0][-]CS_seq _ x n); eauto with arith. astepr (CS_seq _ y n[-][0]); eauto with arith. left. exists (Nat.max Nx Ny); exists (ex[*]ey). apply mult_resp_pos; auto. intros; simpl in |- *; rstepr (CS_seq _ x n[*][--] (CS_seq _ y n)). apply mult_resp_leEq_both; try (apply less_leEq; assumption). astepr (CS_seq _ x n[-][0]); eauto with arith. astepr ([0][-]CS_seq _ y n); eauto with arith. right. exists (Nat.max Nx Ny); exists (ex[*]ey). apply mult_resp_pos; auto. intros; simpl in |- *; astepr (CS_seq _ x n[*]CS_seq _ y n). apply mult_resp_leEq_both; try (apply less_leEq; assumption). astepr (CS_seq _ x n[-][0]); eauto with arith. astepr (CS_seq _ y n[-][0]); eauto with arith. Qed.
imports: CoRN.algebra.COrdCauchy CoRN.tactics.RingReflection