proposition: Lemma Z_gtb_gt: forall a b: Z, Z.gtb a b <-> Z.gt a b.
proof: Proof. split. - rewrite /is_true Z.gtb_lt. now apply Z.lt_gt. - rewrite /is_true Z.gtb_lt. now apply Z.gt_lt. Qed.
imports: Bool Setoid Lia BinInt BinNat PeanoNat ssreflect ssrbool