proposition: Lemma Vmax_cast : forall n (v : nats n) p (e : n=p), Vmax (Vcast v e) = Vmax v.
proof: Proof. induction v; destruct p; intros; try lia. rewrite Vcast_refl. refl. rewrite Vcast_cons. simpl. rewrite IHv. refl. Qed.
imports: CoLoR(VecUtil NatUtil LogicUtil)