proposition: Lemma null_lcos_eql : forall lp l a, Lcos lp l a -> Q_CongA_Null_Acute a -> EqL l lp.
proof: Proof. intros. unfold Lcos in H. spliter. ex_and H3 A. ex_and H4 B. ex_and H3 C. unfold Q_CongA_Null_Acute in H0. spliter. assert(HH:= H7 B A C H6). assert(Col A B C) by (apply out_col;auto). assert(Col C B A) by Col. assert(HQ:= l8_9 C B A H3 H9). induction HQ. subst C. apply (all_eql A B). split; auto. split; auto. subst B. exfalso. unfold Out in HH. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles