proposition: Lemma eqv_permut : forall A B C D, EqV A B C D -> EqV A C B D.
proof: Proof. intros. induction (eq_dec_points A C). subst C. assert(B = D). apply (vector_uniqueness A). assumption. subst D. apply eqv_trivial. unfold EqV in *. induction H. left. apply plg_permut. apply plg_comm2. assumption. left. spliter. subst B. subst D. apply plg_trivial. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec