proposition: Lemma proj_trans : transitive succ -> transitive proj_ord.
proof: Proof. intro. unfold transitive, proj_ord. intros. eapply H. apply H0. hyp. Qed.
imports: CoLoR(ATrs NatUtil BoolUtil VecUtil ListUtil LogicUtil RelUtil SN ACompat ARelation EqUtil)