blob: 6bc165d406f08177752d7d37c830503c827f7a77 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
Require Import Ring.
Require Import ArithRing.
Fixpoint eq_nat_bool (x y : nat) {struct x} : bool :=
match x, y with
| 0, 0 => true
| S x', S y' => eq_nat_bool x' y'
| _, _ => false
end.
Theorem eq_nat_bool_implies_eq : forall x y, eq_nat_bool x y = true -> x = y.
Proof.
induction x; destruct y; simpl; intro H; try (reflexivity || inversion H).
apply IHx in H; rewrite H; reflexivity.
Qed.
Add Ring MyNatSRing : natSRth (decidable eq_nat_bool_implies_eq).
Goal 0 = 0.
ring.
Qed.
|
