proposition: Lemma Rinv_eq_1 : forall a, a <> 0 -> a / a = 1.
proof: Proof. intros. field ; assumption. Qed.
imports: PeanoNat Reals Rintegral Rintegral_usual Rintegral_tactic Lia Lra Rsequence_facts Rsequence_subsequence Rpser RTaylor MyRfunctions Rsequence_tactics