proposition: Lemma Lge_is_eq : forall f a b, (@Lgt f%) a b <-> a = b.
proof: Proof. fo. Qed.
imports: CoLoR(ATrs AInterpretation BoolUtil LogicUtil EqUtil VecUtil SN RelUtil AWFMInterpretation NaryFunction NatUtil ARelation ARules SetUtil FunUtil VecMax AMorphism) Coq(List)