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