proposition: Lemma ex_eqL : forall l1 l2, Q_Cong l1 -> Q_Cong l2 -> (exists A, exists B, l1 A B /\ l2 A B) -> EqL l1 l2.
proof: Proof. intros. ex_and H1 A. ex_and H2 B. unfold EqL. assert(HH1:= H). assert(HH2:= H0). unfold Q_Cong in HH1. unfold Q_Cong in HH2. ex_and HH1 A1. ex_and H3 B1. ex_and HH2 A2. ex_and H3 B2. repeat split; auto. intro. assert(HH:= H4 A0 B0). assert(HP:= H5 A0 B0). destruct HP. apply H6. assert(HP:= H4 A B). assert(HQ:= H5 A B). destruct HP. destruct HQ. apply H9 in H1. apply H11 in H2. destruct HH. apply H13 in H3. apply cong_transitivity with A B; trivial. apply cong_transitivity with A1 B1; Cong. intro. assert(HH:= H4 A0 B0). assert(HP:= H5 A0 B0). destruct HH. apply H6. assert(HH:= H4 A B). assert(HQ:= H5 A B). destruct HH. destruct HQ. apply H9 in H1. apply H11 in H2. destruct HP. apply H13 in H3. apply cong_transitivity with A2 B2; trivial. apply cong_transitivity with A B; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1 Setoid