Helper

lt_minpq_coprime

Section fiber_nd

Type Lemma

Proof Lines 14

Lemma lt_minpq_coprime (a : msg) : (0 < val a)%N -> (val a < minn p q)%N -> coprime (val a) m.

0 < u < min(p,q) implies u is coprime to m = p*q

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...