proposition: Lemma isapropiscommonhzdiv ( k n m : hz ) : isaprop ( iscommonhzdiv k n m ).
proof: Proof. intros. unfold isaprop. apply isofhleveldirprod. - apply hzdiv. - apply hzdiv. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble