proposition: Lemma properT A : (A \proper setT) = (A != setT).
proof: Proof. by rewrite properEneq subsetT andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)