proposition: Lemma exp_mult_card_exp (a b c : Card) : exp_card (b * c) a = exp_card c (exp_card b a).
proof: Proof. rewrite (@commutativity _ _ (.*.) _ b c). reduce. symmetry. apply equiv_uncurry. Defined.
imports: HoTT.TruncType HoTT.Classes.interfaces.abstract_algebra