proposition: Lemma null_lcos : forall l a,Q_Cong l -> ~ Q_Cong_Null l -> Q_CongA_Null_Acute a -> Lcos l l a.
proof: Proof. intros. unfold Q_CongA_Null_Acute in H1. spliter. assert(HH:=ex_points_anga a H1). ex_and HH A. ex_and H3 B. ex_and H4 C. assert(HH:=H2 A B C H3). unfold Lcos. repeat split; auto. assert(B <> A). unfold Out in HH. spliter. auto. lg_instance l A' B'. assert(HP:=ex_point_lg_out l B A H4 H H0). ex_and HP P. exists B. exists P. exists P. repeat split; auto. apply l8_2. apply l8_5. apply (anga_out_anga _ A _ C); auto. apply l6_6. auto. apply (l6_7 _ _ A); apply l6_6. auto. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms