proposition: Lemma mat_ge_dec : forall m n, rel_dec (@mat_ge m n).
proof: Proof. intros R Q. unfold mat_ge. apply mat_forall2_dec. exact ge_dec. Defined.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)