proposition: Lemma cube3_encode_decode o c1 c2 : o2N o - 2 = 0 -> c2N c1 - 2 = 0 -> cube3_decode (cube3_encode o c1 c2) = (o, c1, c2).
proof: Proof. case o; case c1; case c2; simpl; auto; intros; try discriminate. Qed.
imports: ZArith List