proposition: Lemma ang_const : forall a A B, Q_CongA a -> A <> B -> exists C, a A B C.
proof: Proof. intros. unfold Q_CongA in H. ex_and H A0. ex_and H1 B0. ex_and H C0. apply(swap_diff) in H1. assert(HH:= H2 A0 B0 C0). destruct HH. assert(a A0 B0 C0). apply H3. apply conga_refl; auto. assert(HH :=not_col_exists A B H0). ex_and HH P. induction(eq_dec_points A0 C0). subst C0. exists A. assert(HH:= (H2 A B A)). destruct HH. apply H7. apply conga_trivial_1; auto. assert(HH:=angle_construction_2 A0 B0 C0 A B P H H7 H1). ex_and HH C; auto. exists C. apply H2. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid