proposition: Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}.
proof: Proof. intro n; induction n as [|n IHn]; intro m; destruct m; simpl. - left; trivial. - right; intro; trivial. - right; intro; trivial. - apply IHn. Defined.
imports: PeanoNat