proposition: Lemma leb_le n m : (n <=? m) = true <-> n <= m.
proof: Proof. unfold leb, le. destruct compare; easy'. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass