proposition: Lemma cong_inner_transitivity : cong_inner_transitivityP Point cong'.
proof: Proof. move => a b c d e f /andP[H10 H11] /andP[H20 H21]; rewrite /cong'; apply /andP; split; [move: H10 H20|move: H11 H21]; apply cong_inner_transitivity. 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) mathcomp(zmodp) GeoCoq.Meta_theory.Models.POF_to_Tarski GeoCoq.Meta_theory.Counter_models.Planar.independence