proposition: Lemma gtC_wf : WF gtC.
proof: Proof. apply WF_inverse. apply WF_gt. Qed.
imports: CoLoR(LogicUtil OrdUtil LSimple RelUtil) Coq(Structures.Equalities Lia) Coq(Compare_dec) CoLoR(VecUtil) CoLoR(LCompRewrite) CoLoR(SN LCall)