proposition: Lemma bigN_le_gt_dec : forall n m, {n <= m} + {n > m}.
proof: Proof. intros. unfold le, lt. destruct (Z_le_gt_dec [n] [m]). left. hyp. right. unfold Z.lt. rewrite <- Zcompare_antisym, g. refl. Defined.
imports: CoLoR(LogicUtil) Coq(DoubleType) CoLoR(EqUtil) CoLoR(OrdUtil)