proposition: Lemma positive_dec (p1 p2 : positive) : {p1 = p2} + {p1 <> p2}.
proof: Proof. generalize (positive_eq_correct p1 p2). case positive_eq; try (left; auto; fail); right; auto. Defined.
imports: PrimInt63 Cyclic63 List BasicRubik Max