proposition: Lemma trapeze_complet_expl : 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 -> vec C A = vec D B /\ vec C A = vec I J \/ concours_3 A C B D J I.
proof: Proof. intros A B C D I J H10 H11 H H0 H1; try assumption. unfold concours_3, vec in |- *; intros. elim trapeze_complet_PP with (A := A) (B := B) (C := C) (D := D) (I := I) (J := J); [ intros k H2 | auto | auto | auto | auto | auto ]. elim H2; intros H3 H4; try clear H2; try exact H3. elim (classic (k = -1)); intros. rewrite H2 in H3. rewrite H2 in H4. left; try assumption. split; [ try assumption | idtac ]. RingPP1 H3; RingPP. RingPP1 H4; RingPP. right; try assumption. cut (1 + k <> 0); intros. rewrite add_PP_barycentre in H4; auto. rewrite add_PP_barycentre in H4; auto. rewrite add_PP_barycentre in H3; auto. rewrite add_PP_barycentre in H3; auto. exists (barycentre (cons 1 A) (cons k C)). split; [ apply barycentre_alignes; auto | idtac ]. split; [ try assumption | idtac ]. replace (barycentre (cons 1 A) (cons k C)) with (barycentre (cons 1 B) (cons k D)). apply barycentre_alignes; auto. apply conversion_PP with (a := 1 + k) (b := 1 + k); auto. replace (barycentre (cons 1 A) (cons k C)) with (barycentre (cons 1 J) (cons k I)). apply barycentre_alignes; auto. apply conversion_PP with (a := 1 + k) (b := 1 + k); auto. unfold not in |- *; intros; apply H2. replace k with (-1 + (1 + k)). rewrite H5; ring. ring. Qed.