proposition: Lemma R_mult_resp_lt : forall x y, Rlt [0] x -> Rlt [0] y -> Rlt [0] (x[*]y).
proof: Proof. intros x y Hx Hy. elim Hx; intros Nx HN; elim HN; clear Hx HN; intros ex Hex HNx; simpl in HNx; elim Hy; intros Ny HN; elim HN; clear Hy HN; intros ey Hey HNy; simpl in HNy. 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