proposition: Lemma lcos_lg_not_null: forall l lp a, Lcos l lp a -> ~ Q_Cong_Null l /\ ~ Q_Cong_Null lp.
proof: Proof. intros. unfold Lcos in H. spliter. ex_and H2 A. ex_and H3 B. ex_and H2 C. assert(HH:= anga_distinct a B A C H1 H5). spliter. unfold Q_Cong_Null. split; intro; spliter; ex_and H9 X. assert (Cong A B X X) by (apply (lg_cong l); auto). treat_equalities;intuition. assert(Cong A C X X) by (apply (lg_cong lp); auto). treat_equalities;intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles