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