-change with
- (match ((m \sup (S n1) *n) \mod m) with
- [ O \Rightarrow
- match (p_ord_aux m1 ((m \sup (S n1) *n) / m) m) with
- [ (pair q r) \Rightarrow pair nat nat (S q) r]
- | (S a) \Rightarrow pair nat nat O (m \sup (S n1) *n)]
- = pair nat nat (S n1) n).