x := match x with | 0%nat => 0 | S k => k end. Global Instance S_inj : IsInjective@{N N} S := { injective := fun a b E => ap E }. Global Instance nat_dec: DecidablePaths@{N} nat. Proof. hnf. apply (nat_rect@{N} (fun x => forall y, _)). - intros [|b]. + left;reflexivity. + right;apply symmetric_neq,S_neq_0. - intros a IHa [|b]. + right;apply S_neq_0. + destruct (IHa b). * left. apply ap;trivial. * right;intros E. apply (injective S) in E. auto. Defined.
Require Import