proposition: Lemma cong_inner_transitivityT : forall A B C D E F, CongG A B C D -> CongG A B E F -> CongG C D E F.
proof: Proof. intros A B C D E F HCong1 HCong2. apply cong_inner_transitivityG with A B; apply g2_2; auto. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le