proposition: Lemma cube_compare_correct c1 c2 : match cube_compare c1 c2 with | Eq => c1 = c2 | Lt => (c2N c1 < c2N c2)%nat | Gt => (c2N c1 > c2N c2)%nat end.
proof: Proof. case c1; case c2; simpl; auto with arith. Qed.
imports: ZArith List