proposition: Lemma gtb_ltb n m : (n >? m) = (m <? n).
proof: Proof. unfold gtb, ltb. rewrite compare_antisym. now case compare. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass