proposition: Lemma lcos3_lg_not_null: forall lp l a b c, Lcos3 lp l a b c -> ~ Q_Cong_Null l /\ ~ Q_Cong_Null lp.
proof: Proof. intros. unfold Lcos3 in H. ex_and H la. ex_and H0 lab. apply lcos_lg_not_null in H. apply lcos_lg_not_null in H1. spliter. split; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms