proposition: Lemma lcos_lg_distincts : forall lp l a A B C, Lcos lp l a -> l A B -> lp B C -> a A B C -> A <> B /\ C <> B.
proof: Proof. intros. assert(HH:= lcos_lg_not_null lp l a H). spliter. unfold Q_Cong_Null in *. split. intro. subst B. apply H4. unfold Lcos in H. split. tauto. exists A. auto. intro. subst C. apply H3. unfold Lcos in H. split. tauto. exists B. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_3_angles Morphisms