proposition: Lemma lcos2_exists' : forall l a b, Q_Cong l -> ~ Q_Cong_Null l -> Q_CongA_Acute a -> Q_CongA_Acute b -> exists la, exists lab, Lcos la l a /\ Lcos lab la b.
proof: Proof. intros. assert(HH:=lcos_exists l a H1 H H0). ex_and HH la. exists la. apply lcos_lg_anga in H3. spliter. assert(HP:=lcos_not_lg_null la l a H3). assert(HH:=lcos_exists la b H2 H5 HP). ex_and HH lab. exists lab. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms