an attempt to use canonical structures with something else than a type

slides3_3.v

+Require Import Arith.
+
+Structure even_nat := Mkev {enval : nat; _ : Nat.Even enval}.
+
+Lemma even_nat_proof (en : even_nat) : Nat.Even (enval en).
+Proof. destruct en; assumption. Qed.
+
+Lemma decompose_even (en : even_nat) : enval en = 2 * (Nat.div2 (enval en)).
+Proof.
+rewrite <- Nat.double_twice.
+rewrite <- Nat.Even_double.
+  easy.
+now apply even_nat_proof.
+Qed.
+
+Lemma ev_S_proof (en : even_nat) : Nat.Even (S (S (enval en))).
+Proof.
+destruct en as [v Pv].
+simpl.
+rewrite Nat.Even_succ_succ.
+assumption.
+Qed.
+
+Canonical ev_S (en : even_nat) := Mkev (S (S (enval en))) (ev_S_proof en).
+Search Nat.Even 0.
+
+Lemma even0 : Nat.Even 0.
+Proof. exists 0; reflexivity. Qed.
+
+Canonical ev_0 := Mkev 0 even0.
+
+Print Canonical Projections.