proposition: Lemma eqv_refl : forall A B, EqV A B A B.
proof: Proof. intros. unfold EqV. induction (eq_dec_points A B). right. split; auto. left. right. apply plgf_trivial. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec