-(\lambda n,m:nat. if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
-intro.whd.apply le_O_n.intro.whd.apply le_Sn_O.
-
-intros 2.
-simplify.
-cut ((
-
-\lambda b:bool. [\lambda x:bool.Prop] match b:bool with
-[ true \Rightarrow (le n1 m1)
-| false \Rightarrow (Not(le n1 m1))]
-
-\to
-
- [\lambda x:bool.Prop] match b:bool with
-[ true \Rightarrow (le (S n1) (S m1))
-| false \Rightarrow (Not(le (S n1) (S m1)))]
-) (leb n1 m1)).
-goal 8.
-
-exact (
-[
-\lambda b:bool. [\lambda x:bool.Prop] match b:bool with
-[ true \Rightarrow (le n1 m1)
-| false \Rightarrow (Not(le n1 m1))]
-
-\to
-
- [\lambda x:bool.Prop] match b:bool with
-[ true \Rightarrow (le (S n1) (S m1))
-| false \Rightarrow (Not(le (S n1) (S m1)))]
-
-]
-match (leb n1 m1) : bool with
-[ true \Rightarrow \lambda p:(le n1 m1). le_n_S n1 m1 p
-| false \Rightarrow \lambda p:(Not(le n1 m1)). \lambda q:(le (S n1) (S m1)).p(le_S_n n1 m1 q)]
-).
-apply Hcut.
-
-
-cut (eq bool (leb n1 m1) (leb (S n1) (S m1))).
-goal 8.
-simplify.apply refl_equal.
-cut
- (if_then_else
- (leb (S n1) (S m1))
- (le (S n1) (S m1))
- (Not (le (S n1) ( S m1)) )).
-apply Hcut1.elim Hcut.simplify.
-check ([\lambda b:bool. [\lambda b:bool.Prop]match (b:bool) with
- [ true \Rightarrow
- (if_then_else b (le n1 m1) (Not (le n1 m1)))
- | false \Rightarrow
- (if_then_else b (le n1 m1) (Not (le n1 m1)))
-]
-]
-match (leb n1 m1) : bool with
-[ true \Rightarrow H | false \Rightarrow H ]).
-
-
-exact (
-[\lambda b:bool. match (b:bool) with
- [ true \Rightarrow
- (if_then_else b (le (S n1 ) (S m1)) (Not ((le (S n1) (S m1)))))
- | false \Rightarrow
- (if_then_else b (le (S n1 ) (S m1)) (Not ((le (S n1) (S m1)))))
-]
-]
-match (leb n1 m1) : bool with
-[ true \Rightarrow le_n_S n1 m1 H
-| false \Rightarrow
- (\lambda p:(le (S n1) (S m1)).H (le_S_n n1 m1 p))]).
-
-
-
-
-elim n.simplify.apply le_O_n.elim m.
-simplify.apply le_Sn_O.simplify.
-cut (match (leb e e1):bool with
-[true \Rightarrow (eq bool (leb e e1) true)
-| false \Rightarrow (eq bool (leb e e1) false)]).
-goal 20.
-exact [\lambda b:bool. match b with
-[true \Rightarrow (eq bool b true)
-| false \Rightarrow (eq bool b false)]] match (leb e e1):bool with
-[true \Rightarrow refl_equal bool true
-| false \Rightarrow refl_equal bool false].
\ No newline at end of file
+(\lambda n,m:nat.if_then_else (leb n m) (le n m) (Not (le n m))) ? ? ? n m).
+simplify.intros.apply le_O_n.
+simplify.exact le_Sn_O.
+intros 2.simplify.elim (leb n1 m1).
+simplify.apply le_n_S.apply H.
+simplify.intros.apply H.apply le_S_n.assumption.
+qed.
+
+theorem prova :
+let three \def (S (S (S O))) in
+let nine \def (times three three) in
+let eightyone \def (times nine nine) in
+let square \def (times eightyone eightyone) in
+(eq nat square O).
+intro.
+intro.
+intro.intro.
+STOP normalize goal at (? ? % ?).
+
+