proposition: Lemma lg_cong_lg : forall l A B C D, Q_Cong l -> l A B -> Cong A B C D -> l C D.
proof: Proof. intros. unfold Q_Cong in H. ex_and H A0. ex_and H2 B0. assert(HP:= H A B). assert(HQ:= H C D). destruct HP. destruct HQ. apply H4. eapply cong_transitivity. apply H3. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1