proposition: Lemma add_PP_vecteur_rec : forall (a b : R) (A B C M : PO), a + b <> 0 -> add_PP (mult_PP a (vec M A)) (mult_PP b (vec M B)) = mult_PP (a + b) (vec M C) -> add_PP (cons a A) (cons b B) = cons (a + b) C.
proof: Proof. unfold vec in |- *; intros. repeat rewrite <- distrib_mult_cons in H0; auto. replace a with (a * 1); try ring; auto. rewrite calcul in H0. replace b with (b * 1). RingPP2 H0. RingPP. ring. Qed.