proposition: Lemma g2_1 : forall A B, CongG A B A B.
proof: Proof. intros A B. apply cong_inner_transitivityG with B A; apply cong_pseudo_reflexivityG; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le