5 Tactic Definition Arith0 x :=
6 Replace (S x) with (plus (1) x); XAuto.
8 Tactic Definition Arith1 x :=
9 Replace x with (plus x (0)); [XAuto | Auto with arith].
11 Tactic Definition Arith1In H x :=
12 XReplaceIn H x '(plus x (0)).
14 Tactic Definition Arith2 x :=
15 Replace x with (plus (0) x); XAuto.
17 Tactic Definition Arith3 x :=
18 Replace (S x) with (S (plus (0) x)); XAuto.
20 Tactic Definition Arith3In H x :=
21 XReplaceIn H '(S x) '(S (plus (0) x)).
23 Tactic Definition Arith4 x y :=
24 Replace (S (plus x y)) with (plus (S x) y); XAuto.
26 Tactic Definition Arith4In H x y :=
27 XReplaceIn H '(S (plus x y)) '(plus (S x) y).
29 Tactic Definition Arith4c x y :=
30 Arith4 x y; Rewrite plus_sym.
32 Tactic Definition Arith5 x y :=
33 Replace (S (plus x y)) with (plus x (S y)); Auto with arith.
35 Tactic Definition Arith5In H x y :=
36 XReplaceIn H '(S (plus x y)) '(plus x (S y)); Auto with arith.
38 Tactic Definition Arith5' x y :=
39 Replace (plus x (S y)) with (S (plus x y)); Auto with arith.
41 Tactic Definition Arith5'In H x y :=
42 XReplaceIn H '(plus x (S y)) '(S (plus x y)); Auto with arith.
44 Tactic Definition Arith5'c x y :=
45 Arith5' x y; Rewrite plus_sym.
47 Tactic Definition Arith6In H x y :=
48 XReplaceIn H '(plus x (S y)) '(plus (1) (plus x y));
49 [ Idtac | Simpl; Auto with arith ].
51 Tactic Definition Arith7 x :=
52 Replace (S x) with (plus x (1));
53 [ Idtac | Rewrite plus_sym; Auto with arith ].
55 Tactic Definition Arith7In H x :=
56 XReplaceIn H '(S x) '(plus x (1)) ;
57 [ Idtac | Rewrite plus_sym; Auto with arith ].
59 Tactic Definition Arith7' x :=
60 Replace (plus x (1)) with (S x);
61 [ Idtac | Rewrite plus_sym; Auto with arith ].
63 Tactic Definition Arith8 x y :=
64 Replace x with (plus y (minus x y));
65 [ Idtac | Auto with arith ].
67 Tactic Definition Arith8' x y :=
68 Replace (plus y (minus x y)) with x;
69 [ Idtac | Auto with arith ].
71 Tactic Definition Arith9'In H x :=
72 XReplaceIn H '(S (plus x (0))) '(S x).
74 Tactic Definition Arith10 x :=
75 Replace x with (minus (S x) (1));
76 [ Idtac | Simpl; Rewrite <- minus_n_O; Auto with arith ].