proposition: Lemma not_null_ang_def_equiv : forall a, Q_CongA_nNull a <-> (Q_CongA a /\ exists A, exists B, exists C, a A B C /\ ~Out B A C).
proof: Proof. intros. split. intro. unfold Q_CongA_nNull in H. spliter. assert(HH:= H). unfold Q_CongA in HH. ex_and HH A. ex_and H1 B. ex_and H2 C. split. auto. exists A. exists B. exists C. assert(HH:= H3 A B C). destruct HH. assert(a A B C). apply H4. apply conga_refl; auto. split. auto. apply (H0 A B C). auto. intros. spliter. ex_and H0 A. ex_and H1 B. ex_and H0 C. unfold Q_CongA_nNull. split; auto. intros. assert(CongA A0 B0 C0 A B C). apply (ang_conga a); auto. intro. apply H1. apply (l11_21_a A0 B0 C0); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid