proposition: Lemma beq_S_leb x n : (Nat.eqb x (S n) || Compare_dec.leb x n)%bool = Compare_dec.leb x (S n).
proof: Proof. revert x; induction n as [|n IHn]; simpl. { intros [|[|]]; reflexivity. } { intros [|x]; [ reflexivity | apply IHn ]. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith