proposition: Lemma D_minus_compat : forall f g, D (f - g)%F == (D f - D g)%F.
proof: Proof. intros f g x ; unfold D, minus_fct, Rminus ; ring. Qed.
imports: Rsequence_def Rsequence_sums_facts Rsequence_rewrite_facts MyNat Rfunction_def