proposition: Lemma permut_cons : forall h p q, permut p q -> permut (h :: p) (h :: q).
proof: Proof. intros h p q. apply (permut_app_l (h :: nil)). Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)