Helper

dsdp_fiber_card

Section dsdp_entropy

Type Lemma

Proof Lines 5

Lemma dsdp_fiber_card (u1 u2 u3 v1 s : msg) : (0 < u3)%N -> (u3 < minn p q)%N -> #|dsdp_fiber u1 u2 u3 v1 s| = m.

Fiber cardinality for full constraint

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

No lemmas in the stats use this lemma.

Loading source code...