proposition: Lemma Vanprod_anti n (R : comRingType) : @Vanprod n R \is antisym.
proof: Proof. case: n => [| n]. by apply/isantisymP => s; rewrite (permS0 s) msym1m odd_perm1 simplexp. apply/isantisym_eltrP => i Hi. rewrite /Vanprod. rewrite (bigD1 (inord i, inord i.+1)) /=; first last. by rewrite !inordK //=; apply (leq_trans Hi). rewrite msymM -mulNr; congr (_ * _). rewrite msymB opprB. by congr (_ - _); rewrite /msym mmapX mmap1U ?eltrL ?eltrR. rewrite (big_morph _ (msymM 's_i) (msym1 _ 's_i)) /=. under [LHS]eq_bigr do rewrite msymB /msym !mmapX !mmap1U. under [LHS]eq_bigl => p do rewrite -/(predi i p) (predi_eltrpE p Hi). rewrite /= -(big_map _ _ (fun p => ('X_p.1 - 'X_p.2))) /=. set L := map _ _; suff Hin : perm_eq L (enum {: 'II_ n.+1}). by rewrite (perm_big _ Hin) big_enum_cond. apply: uniq_perm. - rewrite {}/L map_inj_uniq; first exact: index_enum_uniq. exact: (can_inj (eltrpK _)). - exact: enum_uniq. - rewrite /L => [[u v]]; rewrite mem_enum inE. rewrite -(eltrpK i (u,v)). by apply map_f; rewrite mem_index_enum. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm zmodp binomial) mathcomp(ssrcomplements freeg mpoly) tools permcomp presentSn sorted partition