proposition: Lemma D_x_no_cond : forall x a:R, a <> 0 -> D_x no_cond x (x + a).
proof: Proof. intros. unfold D_x, no_cond. split. - trivial. - apply Rminus_not_eq. unfold Rminus. rewrite Ropp_plus_distr. rewrite <- Rplus_assoc. rewrite Rplus_opp_r. rewrite Rplus_0_l. apply Ropp_neq_0_compat; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 Lra