proposition: Theorem lap_eq_cons_inv : ∀ α (r : ring α) x₁ x₂ l₁ l₂, lap_eq [x₁ … l₁] [x₂ … l₂] → (x₁ = x₂)%K ∧ lap_eq l₁ l₂.
proof: Proof. intros α r x₁ x₂ l₁ l₂ H. inversion H; split; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation