proposition: Lemma Derivative_I_scal : forall c : IR, Derivative_I Hab' (c{**}F) (c{**}F').
proof: Proof. intro. unfold Fscalmult in |- *. apply Derivative_I_wdr with ([-C-]c{*}F'{+}[-C-][0]{*}F). FEQ. Deriv. Qed.
imports: CoRN.ftc.Derivative