blob: 4cc0f9cbf848a5a81ffd1eea7396cace42364e0c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp
Require Import ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
(* error 1 *)
Ltac subst1 H := move: H ; rewrite {1} addnC; move => H.
Ltac subst2 H := rewrite addnC in H.
Goal ( forall a b: nat, b+a = 0 -> b+a=0).
Proof. move => a b hyp. subst1 hyp. subst2 hyp. done. Qed.
|
