proposition: Lemma between_identityT : forall A B, BetG A B A -> A = B.
proof: Proof. intros A B; apply g2_16 with GPA GPB GPC; intro HNBet; apply lower_dimG; left; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le