proposition: Lemma cong_inner_transitivity' : forall A B C D E F, Cong A B E F -> Cong C D E F -> Cong A B C D.
proof: Proof. intros A B C D E F H1 H2; apply (cong_inner_transitivity E F); apply cong_symmetry; assumption. Qed.
imports: GeoCoq.Axioms.tarski_axioms GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Tarski_dev.Ch05_bet_le