lean2/examples/lean/ex4.lean

6 lines
193 B
Text
Raw Normal View History

Definition a : Nat := 10
(* Trivial indicates a "proof by evaluation" *)
Theorem T1 : a > 0 := Trivial
Theorem T2 : a - 5 > 3 := Trivial
(* The next one fails *)
Theorem T3- : a > 11 := Trivial