- #n; nelim n
- [ @1; nnormalize; @1
- | #m; #H; @2
- [ nnormalize; @1
- | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
- nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
- #E; nrewrite > E; nassumption ]##]
+ #n; nelim n; /2/;
+ #m; nelim m; nnormalize
+ [ #H; @2; nnormalize; ##[//;##] (* XXX: bug auto *)
+ #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; //
+ ##| #p; #H1; #H2; @2; nnormalize; //;
+ #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
+ nrewrite < (plus_n_Sm …); // ]