proposition: Lemma helper (P : nat -> nat -> Type) n (H0 : forall n0, P (min 1 (n - n0)) n0) (H1 : forall n0, P 1 (n0 + n)) {n0} : P 1 n0.
proof: Proof. destruct (Compare_dec.le_dec n n0) as [H'|H']. { specialize (H1 (n0 - n)). rewrite Nat.sub_add in H1 by assumption; assumption. } { apply Compare_dec.not_le in H'. specialize (H0 n0). destruct (n - n0) as [|[|]] eqn:?; simpl in *; trivial; omega. } Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common