proposition: Lemma add_PP_alignes : forall (a b : R) (A B C : PO), a + b <> 0 -> add_PP (cons a A) (cons b B) = cons (a + b) C -> alignes A B C.
proof: Proof. unfold alignes, alignes1, vec in |- *; intros. right; try assumption. exists (1 + - (/ (a + b) * b)). apply mult_PP_regulier with (a + b); auto. replace (mult_PP (a + b) (cons 1 C)) with (cons (a + b) C); [ idtac | RingPP ]. rewrite <- H0. FieldPP (a + b). Qed.