proposition: Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p).
proof: Proof. induction n as [|n IHn]. - reflexivity. - simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p). Qed.
imports: PeanoNat