proposition: Lemma lcos2_eq_lcos3_eq : forall la lb a b c d e, Q_CongA_Acute e -> Eq_Lcos2 la a b lb c d -> Eq_Lcos3 la a b e lb c d e.
proof: Proof. intros. assert(HH0:=H0). unfold Eq_Lcos2 in HH0. ex_and HH0 lp. apply lcos2_lg_anga in H1. apply lcos2_lg_anga in H2. spliter. assert(~ Q_Cong_Null la /\ ~ Q_Cong_Null lp). eapply (lcos2_lg_not_null _ _ a b). auto. spliter. assert(HH:= lcos_exists lp e H H3 H12). ex_and HH lq. apply lcos_lg_anga in H13. spliter. assert(~ Q_Cong_Null lq /\ ~ Q_Cong_Null lp). apply (lcos_lg_not_null _ _ e); auto. spliter. unfold Eq_Lcos3. exists lq. split; apply lcos3_lcos_2_1; exists lp; split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms