proposition: Lemma l13_10_aux2 : forall O A B la lla lb llb, Col O A B -> Q_Cong la -> Q_Cong lla -> Q_Cong lb -> Q_Cong llb -> la O A -> lla O A -> lb O B -> llb O B -> A <> O -> B <> O -> exists a, Q_CongA_Acute a /\ Lcos lla la a /\ Lcos llb lb a.
proof: Proof. intros. assert(HH:=anga_exists A O A H8 H8 (acute_trivial A O H8)). ex_and HH a. exists a. split; auto. assert(Q_CongA_Null_Acute a). assert(Out O A A /\ Q_CongA_Null_Acute a). apply(anga_col_null a A O A); auto. Col. tauto. split. assert(EqL la lla). apply ex_eql. exists O. exists A. repeat split; auto. rewrite <- H13. apply null_lcos; auto. intro. unfold Q_Cong_Null in H14. spliter. ex_and H15 X. assert(HH:= lg_cong la O A X X H0 H4 H16). treat_equalities. tauto. assert(HH:=anga_exists B O B H9 H9 (acute_trivial B O H9)). ex_and HH b. assert(EqA a b). assert(HH:=null_anga A O B O a b). apply HH; split; auto. assert(EqL lb llb). apply ex_eql. exists O. exists B. repeat split; auto. rewrite <- H16. apply null_lcos; auto. intro. unfold Q_Cong_Null in H17. spliter. ex_and H18 X. assert(HH:= lg_cong lb O B X X H2 H6 H19). treat_equalities. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project