proposition: Lemma inv_id_matrix : vec_invariant (Vreplace (Vconst A0 dim) dim_pos A1).
proof: Proof. unfold vec_invariant, vec_at0. rewrite Vnth_replace. exact A0_gt_A1. Qed.
imports: CoLoR(AMonAlg Matrix OrdSemiRing VecUtil SN RelUtil LogicUtil AMatrixBasedInt) Coq(Morphisms Setoid)