proposition: Lemma lcos3_lg_anga : forall lp l a b c, Lcos3 lp l a b c -> Lcos3 lp l a b c /\ Q_Cong lp /\ Q_Cong l /\ Q_CongA_Acute a /\ Q_CongA_Acute b /\ Q_CongA_Acute c.
proof: Proof. intros. split; auto. unfold Lcos3 in H. ex_and H la. ex_and H0 lab. apply lcos_lg_anga in H. apply lcos_lg_anga in H0. apply lcos_lg_anga in H1. spliter. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms