proposition: Lemma cong_stability_eq_stability : forall A B : ITpoint, ~ A <> B -> A = B.
proof: Proof. intros A B HAB. apply Icong_identity with A. apply Cong_stability. intro HNCong. apply HAB. intro HEq. subst. apply HNCong. apply Icong_pseudo_reflexivity. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms