proposition: Lemma Cmult_Rinj_algebrique : forall x y k : R, Cmult (Rinj k) (cons_cart x y) = cons_cart (k * x) (k * y).
proof: Proof. unfold Rinj in |- *; intros. rewrite Cmult_algebrique. replace (k * x + - (0 * y)) with (k * x) by ring. replace (0 * x + k * y) with (k * y) by ring. auto. Qed.