proposition: Lemma g2_3 : forall A B C D, CongG A B C D -> CongG B A C D.
proof: Proof. Proof. intros A B C D HCong. apply cong_inner_transitivityT with A B; auto. apply cong_pseudo_reflexivityG. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le