proposition: Lemma lg_null_dec : forall l, Q_Cong l -> Q_Cong_Null l \/ ~ Q_Cong_Null l.
proof: Proof. intros. assert(HH:=H). unfold Q_Cong in H. ex_and H A. ex_and H0 B. induction(eq_dec_points A B). subst B. left. unfold Q_Cong_Null. split. auto. exists A. apply H. Cong. right. intro. unfold Q_Cong_Null in H1. spliter. ex_and H2 P. apply H0. assert(Cong A B P P). apply H; auto. apply cong_identity in H2. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1