proposition: Theorem lap_mul_shuffle0 : ∀ la lb lc, lap_eq (lap_mul (lap_mul la lb) lc) (lap_mul (lap_mul la lc) lb).
proof: Proof. intros la lb lc. do 2 rewrite <- lap_mul_assoc. apply lap_mul_compat; [ reflexivity | apply lap_mul_comm ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation