proposition: Lemma inv_id_matrix : vec_invariant (Vreplace (Vconst A0 dim) dim_pos A1).
proof: Proof. compute. trivial. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)