proposition: Lemma ang_const_o : forall a A B P, ~Col A B P -> Q_CongA a -> Q_CongA_nNull a -> Q_CongA_nFlat a -> exists C, a A B C /\ OS A B C P.
proof: Proof. intros. assert(HH:= H0). unfold Q_CongA in HH. ex_and HH A0. ex_and H3 B0. ex_and H4 C0. apply(swap_diff) in H4. assert(HH:= H5 A0 B0 C0). destruct HH. assert(a A0 B0 C0). apply H6. apply conga_refl; auto. assert(HH:=ang_distincts a A0 B0 C0 H0 H8). assert(A0 <> C0). intro. subst C0. unfold Q_CongA_nNull in H1. spliter. assert(HH:=H11 A0 B0 A0 H8). apply HH. apply out_trivial; auto. spliter. assert(A <> B). intro. subst B. apply H. Col. assert(HH:=angle_construction_2 A0 B0 C0 A B P H10 H9 H4). ex_and HH C; auto. exists C. assert(a A B C). assert(HH:= H5 A B C). destruct HH. apply H15. auto. split. auto. induction H14. auto. unfold Q_CongA_nNull in H1. spliter. assert(HH:= H16 A B C H15). unfold Q_CongA_nFlat in H2. spliter. assert(Hh:=H17 A B C H15). apply False_ind. assert(HH0:=ang_distincts a A B C H0 H15). spliter. assert(HP:=or_bet_out A B C). induction HP. contradiction. induction H20. contradiction. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid