proposition: Lemma and10P : reflect [/\ b1, b2, b3, b4, b5, b6, b7, b8, b9 & b10] [&& b1, b2, b3, b4, b5, b6, b7, b8, b9 & b10].
proof: Proof. case: b1=>/=; last by constructor; case. case: b2=>/=; last by constructor; case. case: b3=>/=; last by constructor; case. case: b4=>/=; last by constructor; case. case: b5=>/=; last by constructor; case. case: b6=>/=; last by constructor; case. case: b7=>/=; last by constructor; case. case: b8=>/=; last by constructor; case. case: b9=>/=; last by constructor; case. case: b10=>/=; last by constructor; case. by constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)