proposition: Lemma cong_v_aabc a b c : cong_v (#a) (#a) (#b) (#c) = ((#b) == (#c)).
proof: Proof. apply /eqP /eqP. move=>/eqP. rewrite eq_sym -/(cong_v _ _ _ _) -/(cong' _ _ _ _) => H. rewrite (@cong_identity b c a) //. move->. rewrite -!expr2 -!/(omd _ _) !divff ?mulf_eq0 ?omd_eq0 //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype choice seq) mathcomp(fintype finset finfun bigop order) mathcomp(ssralg ssrnum path generic_quotient matrix mxalgebra algC) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.tarski_to_gupta_inspired GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tarski_dev.Ch11_angles GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Meta_theory.Counter_models.Planar.independence