proposition: Lemma E_in_disk (a b c d : Point) : (exists E' : Vector, bet (#a) (#b) E' /\ cong_v (#b) E' (#c) (#d))-> exists E : Point, bet' a b E /\ cong' b E c d.
proof: Proof. move=> H. destruct H as [E' [bet cong_v]]. assert (E'_in_disk := cong_v). apply E_in_disk_aux in E'_in_disk. set E := (exist (fun p => (p *m p^T) 0 0 < 1) E' E'_in_disk). exists E. by rewrite /bet' bet /cong' cong_v. 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