proposition: Lemma lcos_eq_lcos2_eq : forall la lb a b c, Q_CongA_Acute c -> Eq_Lcos la a lb b -> Eq_Lcos2 la a c lb b c.
proof: Proof. intros. assert(HH0:=H0). unfold Eq_Lcos in HH0. ex_and HH0 lp. apply lcos_lg_anga in H1. apply lcos_lg_anga in H2. spliter. clear H7. assert(~ Q_Cong_Null lp /\ ~ Q_Cong_Null la). apply (lcos_lg_not_null _ _ a). auto. spliter. unfold Eq_Lcos2. assert(HH:= lcos_exists lp c H H4 H7). ex_and HH lq. exists lq. split. unfold Lcos2. exists lp. split; auto. unfold Lcos2. exists lp. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms