proposition: Lemma lcos_eq_lcos3_eq : forall la lb a b c d, Q_CongA_Acute c -> Q_CongA_Acute d -> Eq_Lcos la a lb b -> Eq_Lcos3 la a c d lb b c d.
proof: Proof. intros. assert(HH1:=H1). unfold Eq_Lcos in HH1. ex_and HH1 lp. apply lcos_lg_anga in H2. apply lcos_lg_anga in H3. spliter. assert(~ Q_Cong_Null lp /\ ~ Q_Cong_Null la). apply (lcos_lg_not_null _ _ a). auto. spliter. assert(HH:= lcos_exists lp c H H5 H10). ex_and HH lq. apply lcos_lg_anga in H12. spliter. assert(~ Q_Cong_Null lq /\ ~ Q_Cong_Null lp). apply (lcos_lg_not_null _ _ c); auto. spliter. assert(HH:= lcos_exists lq d H0 H14 H16). ex_and HH lm. unfold Eq_Lcos3. exists lm. split; unfold Lcos3. exists lp. exists lq. split; auto. exists lp. exists lq. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms