proposition: Lemma cong3_transitivity : forall A0 B0 C0 A1 B1 C1 A2 B2 C2, Cong_3 A0 B0 C0 A1 B1 C1 -> Cong_3 A1 B1 C1 A2 B2 C2 -> Cong_3 A0 B0 C0 A2 B2 C2.
proof: Proof. unfold Cong_3. intros. spliter. repeat split; eapply cong_transitivity; eCong. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish