proposition: Lemma i1eqiF i : (i.+1 == i) = false.
proof: Proof. by apply: negbTE; elim i. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr