proposition: Lemma vec_order_strict_wf : forall dim, well_founded (vec_order_strict dim).
proof: Proof. destruct dim as [|dim]. simpl. apply lt_wf. simpl. intros [a v]. revert v. pattern a. apply well_founded_ind with (1:=lt_wf). clear a. intros a1 IHa1 v1. constructor. intros [a2 v2] [H1 _]. apply IHa1 ; assumption. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)