proposition: Lemma vec_order_large_refl dim: forall x, vec_order_large dim x x.
proof: Proof. induction dim. simpl. apply o.(le_refl). simpl;intros [a v];split;[apply o.(le_refl)|apply IHdim]. Defined.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)