proposition: Lemma angle_non_paralleles : forall A B C D : PO, A <> B :>PO -> C <> D :>PO -> double_AV (cons_AV (vec A B) (vec C D)) <> image_angle 0 :>AV -> ~ paralleles (droite C D) (droite A B).
proof: Proof. intros; red in |- *; intros. apply H1; apply angle_droites_paralleles; auto. Qed.