proposition: Lemma eql_lcos_null : forall l lp a, Lcos l lp a -> EqL l lp -> Q_CongA_Null_Acute a.
proof: Proof. intros. unfold Lcos in H. spliter. ex_and H3 B. ex_and H4 A. ex_and H3 C. assert(forall A0 B0 : Tpoint, l A0 B0 <-> lp A0 B0). apply H0; auto. assert(HP:= (H7 B A)). assert(HQ:= (H7 B C)). destruct HP. destruct HQ. assert(l B C). apply H11. auto. assert(lp B A). apply H8. auto. clear H7 H8 H9 H10 H11. assert(Cong B A B C). apply (lg_cong l); auto. unfold Per in H3. ex_and H3 B'. assert(HH:= anga_distinct a A B C H2 H6). spliter. assert(A = C). eapply (l4_18 B B'). intro. subst B'. apply l7_3 in H3. contradiction. unfold Midpoint in H3; assert(HH:= midpoint_col). spliter. apply bet_col in H3. Col. auto. unfold Midpoint in H3. spliter. eapply cong_transitivity. apply cong_symmetry. apply cong_commutativity. apply H11. eapply cong_transitivity. apply cong_commutativity. apply H7. Cong. subst C. unfold Q_CongA_Null_Acute. split. auto. intros A0 B0 C0 HP. apply (eq_conga_out A B). apply (anga_conga a); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles