proposition: Lemma Z_geb_ge: forall a b: Z, Z.geb a b <-> Z.ge a b.
proof: Proof. split. - rewrite /is_true Z.geb_le. now apply Z.le_ge. - rewrite /is_true Z.geb_le. now apply Z.ge_le. Qed.
imports: Bool Setoid Lia BinInt BinNat PeanoNat ssreflect ssrbool