qed.
theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
match p_ord_aux p n m with
[ (pair q r) \Rightarrow r \mod m \neq O].
qed.
theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
match p_ord_aux p n m with
[ (pair q r) \Rightarrow r \mod m \neq O].