The general method in Dafny for proving something by contradiction is:

lemma X() ensures Q(x) { if !Q(x) { // derive contradiction assert false; } } |

The general method in Dafny for proving something by contradiction is:

lemma X() ensures Q(x) { if !Q(x) { // derive contradiction assert false; } } |