proposition: Lemma trapeze_complet_expl2 : 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 D A = vec C B /\ vec D A = vec I J \/ concours_3 A D B C J I.
proof: Proof. intros. elim (trapeze_complet_expl (A:=A) (B:=B) (C:=D) (D:=C) (I:=I) (J:=J)); auto with geo; intros. apply paralleles_trans with (C := C) (D := D); auto with geo. Qed.