proposition: Lemma Rinv_plus : forall a b c : R, c <> 0 -> (a + b) / c = a / c + (b / c).
proof: Proof. intros a b c d. field ; apply d. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics