proposition: Lemma trapeze_complet_PP : forall A B C D I J : PO, A <> B :>PO -> C <> D :>PO -> paralleles (droite A B) (droite C D) -> I = milieu C D -> J = milieu A B -> ex (fun k : R => add_PP (cons 1 A) (cons k C) = add_PP (cons 1 B) (cons k D) :>PP /\ add_PP (cons 1 A) (cons k C) = add_PP (cons 1 J) (cons k I) :>PP).
proof: Proof. intros A B C D I J H10 H11 H H0 H1; try assumption. elim Thales_PP with (3 := H); auto. intros x H2; try assumption. exists x. split; [ try assumption | idtac ]. rewrite H1; rewrite H0. apply mult_PP_regulier with (k := 2); try discrR. repeat rewrite <- distrib_mult_cons. replace (2 * 1) with 2; try ring; auto. rewrite <- add_PP_milieu. replace (2 * x) with (x * 2); try ring; auto. repeat rewrite <- def_mult_PP. rewrite <- add_PP_milieu. replace 2 with (1 + 1) by ring. rewrite <-!add_PP_A. RingPP1 H2. RingPP. Qed.