proposition: Lemma eqv_sym : forall A B C D, EqV A B C D -> EqV C D A B.
proof: Proof. intros. unfold EqV in *. induction H. left. apply plg_sym. apply plg_comm2. assumption. right. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec