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