proposition: Lemma cong_stability : forall A B C D, ~ ~ Cong A B C D -> Cong A B C D.
proof: Proof. intros. elim (cong_dec A B C D); intro HCong. apply HCong. contradiction. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality