proposition: Lemma le_SS n m (H : n <= m) : S n <= S m.
proof: Proof. induction H. { constructor. } { constructor; assumption. } Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Classes.Morphisms Coq.Program.Basics