proposition: Lemma gt_WF : WF gt.
proof: Proof. apply wf_transp_WF. apply well_founded_lt_compat with (fun x => match x with | Pos x => x + 1 | MinusInf => 0 end). intros. destruct x; destruct y; solve [auto with arith | exfalso; auto]. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)