Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive CubeDifference : nat -> Prop :=
- | evidence : forall n m k, CubeDifference (n * n * n - m * m *m - k * k * k).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement