proposition: Theorem lap_add_shuffle0 : ∀ la lb lc, lap_eq (lap_add (lap_add la lb) lc) (lap_add (lap_add la lc) lb).
proof: Proof. intros la lb lc. do 2 rewrite <- lap_add_assoc. apply lap_add_compat; [ reflexivity | simpl ]. apply lap_add_comm. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation