proposition: Lemma beq_0_1_leb x : (Nat.eqb x 1 || Nat.eqb x 0)%bool = Compare_dec.leb x 1.
proof: Proof. destruct x as [|[|]]; simpl; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith