Vladimir Timashov wrote: > Hello. > > I need advice in how to prove following subgoal...
> So please advice. Any help will be greatly appreciated. I think your problems probably stem from the fact that you are working over the natural numbers, where there aren't any negative numbers. So rather than i - 2 = -1 you'll actually have that i - 2 = 0 You could either change to use integers (load "intLib" and use the :int type annotation as necessary); or recast your goal to cope with subtraction better. In your particular goal, i - 2, i - 1 and i might all be zero, preventing the application of your last assumption. Hope this helps, Michael. ------------------------------------------------------------------------- This SF.Net email is sponsored by the Moblin Your Move Developer's challenge Build the coolest Linux based applications with Moblin SDK & win great prizes Grand prize is a trip for two to an Open Source event anywhere in the world http://moblin-contest.org/redirect.php?banner_id=100&url=/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
