proposition: Lemma g2_5 : forall A B C D, CongG A B C D -> (A = B <-> C = D).
proof: Proof. intros A B C D HCong. split; intro H; rewrite H in HCong; [apply g2_2 in HCong|]; apply cong_identityG in HCong; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le