proposition: Lemma is_ang_distinct : forall A B C a , Ang A B C a -> A <> B /\ C <> B.
proof: Proof. intros. unfold Ang in H. spliter. unfold Q_CongA in H. ex_and H A0. ex_and H1 B0. ex_and H C0. assert(HH:= H2 A B C). destruct HH. apply H4 in H0. unfold CongA in H0. spliter. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length