proposition: Lemma neq_sym (T: eqType) (x y: T): (x != y) = (y != x).
proof: Proof. case: (_ =P _); first by move => ->; rewrite eqxx. case: (_ =P _) => // -> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)