proposition: Lemma derg1 A : A^`(1) = [~: A, A].
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)