proposition: Lemma is_above_zero_ok : forall v, is_above_zero v = true <-> ge v (Fin 0).
proof: Proof. intro. destruct v; simpl; intuition. destruct z. right. refl. left. simpl. auto with zarith. discr. rewrite is_not_neg_ok. destruct H. simpl in H. auto with zarith. inversion H. auto with zarith. destruct H. simpl in H. contr. discr. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)