proposition: Lemma eqv_cong : forall A B C D, EqV A B C D -> Cong A B C D.
proof: Proof. intros. unfold EqV in H. induction H. apply plg_cong. apply plg_permut. apply plg_comm2. assumption. spliter. subst B. subst D. Cong. Qed.
imports: GeoCoq.Tarski_dev.Annexes.vectors