proposition: Lemma algebrique_operations : forall x y : R, cons_cart x y = Cplus (Rinj x) (Cmult i (Rinj y)).
proof: Proof. unfold i in |- *; unfold Rinj in |- *; intros. rewrite Cmult_algebrique; rewrite Cplus_algebrique. replace (x + (0 * y + - (1 * 0))) with x; [ idtac | ring ]. replace (0 + (1 * y + 0 * 0)) with y; [ auto | ring ]. Qed.