proposition: Lemma all_cons P Ps: all (P::Ps) ↔ P ∧ all Ps.
proof: Proof. unfold all. revert P; generalize True as Q. induction Ps as [|P' Ps IH]; intros. { cbn; tauto. } change (fold_left and (P' :: Ps) (Q ∧ P) ↔ P ∧ fold_left and (P'::Ps) Q). rewrite !IH. transitivity (P' ∧ (P ∧ fold_left and Ps Q)); try tauto. now rewrite <- (IH Q P). Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.rings Ring