proposition: Lemma diffP {T:eqType}(i j:T): reflect (i <> j) (i != j).
proof: Proof. case E: (i == j) => //=; constructor => H. - have H1: i = j by apply /eqP => //. done. - move: E; by rewrite H eq_refl. Qed.
imports: mathcomp(all_ssreflect zify)