proposition: Proposition nat_add_bifunctor (n n' m m' : nat) : n <= m -> n' <= m' -> n + n' <= m + m'.
proof: Proof. revert n' m m'; simple_induction n n IHn. - intros n' m m' l l'. simpl. apply (leq_trans l'). exact (n_leq_add_n_k' m' m). - intros n' m; destruct m. + intros. contradiction (not_leq_Sn_0 n). + intros m' l l'. apply leq_S_n in l. simpl. apply leq_S_n', IHn. * exact l. * exact l'. Defined.
imports: Basics Spaces.Nat.Core