proposition: Lemma add_PP_concours : forall (a b c d : R) (A B C D I : PO), A <> B :>PO -> C <> D :>PO -> a + b <> 0 :>R -> add_PP (cons a A) (cons b B) = cons (a + b) I :>PP -> c + d <> 0 :>R -> add_PP (cons c C) (cons d D) = cons (c + d) I :>PP -> concours (droite A B) (droite C D).
proof: Proof. intros a b c d A B C D I H H0 H1 H2 H3 H4; try assumption. apply def_concours with I; auto. apply add_PP_alignes with (a := a) (b := b); auto. apply add_PP_alignes with (a := c) (b := d); auto. Qed.