proposition: Lemma tech7 : forall r1 r2:R, r1 <> 0 -> r2 <> 0 -> r1 <> r2 -> / r1 <> / r2.
proof: Proof. intros; red; intro. assert (H3 := Rmult_eq_compat_l r1 _ _ H2). rewrite Rinv_r in H3; [ idtac | assumption ]. assert (H4 := Rmult_eq_compat_l r2 _ _ H3). rewrite Rmult_1_r in H4; rewrite <- Rmult_assoc in H4. rewrite Rmult_inv_r_id_m in H4; [ idtac | assumption ]. elim H1; symmetry ; assumption. Qed.
imports: Rbase Rfunctions Rseries Rcomplete