proposition: Lemma sum_mat_app: forall a b, sum_mat (a++b) = sum_mat a + sum_mat b.
proof: Proof. intros. induction a; unfold sum_mat in *; simpl; [|rewrite IHa]; lia. Qed.
imports: VST.floyd.proofauto CertiGraph.summatrix.summatrix VST.msl.iter_sepcon