proposition: Lemma depair_sanity {m n} (o : t m) (p : t n) : proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
proof: Proof. induction o as [|? o IHo] ; simpl. - rewrite L_sanity. now rewrite Nat.mul_0_r. - rewrite R_sanity. rewrite IHo. rewrite Nat.add_assoc. destruct (to_nat o); simpl; rewrite Nat.mul_succ_r. now rewrite (Nat.add_comm n). Qed.
imports: PeanoNat