proposition: Lemma cong_trivial_identityT : forall A B, CongG A A B B.
proof: Proof. intros A B; destruct (g2_6 B A); auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le