lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉.
#p elim p // #p1 #Hind #n
cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod
lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉.
#p elim p // #p1 #Hind #n
cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod