proposition: Lemma par_strict_distinct : forall A B C D, Par_strict A B C D -> A<>B /\ A<>C /\ A<>D /\ B<>C /\ B<>D /\ C<>D.
proof: Proof. unfold Par_strict. intros; spliter. repeat split; intro; apply H0; [exists C|exists A|exists A|exists B..]; subst; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles