proposition: Lemma le_gt_dec : forall n m, {n <= m} + {n > m}.
proof: Proof. intros. unfold BigZ.le, BigZ.lt. destruct (Z_le_gt_dec (BigZ.to_Z n) (BigZ.to_Z m)). left. hyp. right. unfold Z.lt. rewrite <- Zcompare_antisym, g. refl. Defined.
imports: CoLoR(LogicUtil BigNUtil NatUtil) Coq(ZArith) CoLoR(OrdUtil)