proposition: Lemma lg_cong : forall l A B C D, Q_Cong l -> l A B -> l C D -> Cong A B C D.
proof: Proof. intros. unfold Q_Cong in H. ex_and H X. ex_and H2 Y. assert(HH:= H A B). destruct HH. assert(HH:= H C D). destruct HH. apply H3 in H0. apply H5 in H1. apply cong_transitivity with X Y; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1