proposition: Theorem lap_app_add : ∀ la lb, (la ++ lb = la + list_pad (length la) 0%K lb)%lap.
proof: Proof. intros la lb. induction la as [| a]; [ reflexivity | simpl ]. rewrite rng_add_0_r. constructor; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation