proposition: Lemma eqv_par : forall A B C D, A <> B -> EqV A B C D -> Par A B C D.
proof: Proof. intros. unfold EqV in H0. induction H0. unfold Parallelogram in H0. induction H0. unfold Parallelogram_strict in H0. spliter. apply par_right_comm. assumption. unfold Parallelogram_flat in H0. spliter. right. spliter. repeat split; Col. intro. subst D. apply cong_identity in H2. contradiction. ColR. ColR. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec