proposition: Lemma ex_ang : forall A B C, B <> A -> B <> C -> exists a, Q_CongA a /\ a A B C.
proof: Proof. intros. exists (fun X Y Z => CongA A B C X Y Z). unfold Q_CongA. split. exists A. exists B. exists C. split. auto. split. auto. intros. split. intro. auto. intro. auto. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length