proposition: Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m.
proof: Proof. induction n; intros. - apply add_0_l. - rewrite ofnat_succ, add_succ_l. simpl. now f_equiv. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat