proposition: Lemma ex_anga : forall A B C, Acute A B C -> exists a, Q_CongA_Acute a /\ a A B C.
proof: Proof. intros. exists (fun X Y Z => CongA A B C X Y Z). unfold Q_CongA_Acute. assert (HH := acute_distincts A B C H). spliter. split. exists A. exists B. exists C. split; auto. intros. intros. split. intro. auto. intro. auto. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid