Lemma asMultipleOfMod : forall s q (Hneq : 0 <> q), (asMultipleOf s q Hneq) mod q = 0.
