]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/replace.ma
7117d5b8210b29f4b64d34628eba978f6999d96e
[helm.git] / helm / matita / tests / replace.ma
1 set "baseuri" "cic:/matita/tests/replace/".
2 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
3 alias num (instance 0) = "natural number".
4 alias symbol "eq" (instance 0) = "leibnitz's equality".
5 alias symbol "plus" (instance 0) = "natural plus".
6 alias symbol "times" (instance 0) = "natural times".
7 alias id "mult_n_O" = "cic:/Coq/Init/Peano/mult_n_O.con".
8 alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con".
9
10 theorem t: \forall x:nat. x * (x + 0) = (0 + x) * (x + x * 0).
11  intro.
12  replace in \vdash (? ? (? ? %) (? % %)) with x.
13  reflexivity.
14  rewrite < mult_n_O x.
15  rewrite < plus_n_O x.
16  reflexivity.
17  reflexivity.
18  auto.
19 qed.