proposition: Lemma R_len : forall x y, R x y -> len x > len y.
proof: Proof. intros. rewrite len_eq. unfold gt, lt. apply le_n_S. apply in_lmax. apply in_map. apply R_in_sons. exact H. Qed.
imports: CoLoR(SN ListMax RelUtil ListUtil LogicUtil) Coq(Arith)