Function montgomery_reduction_congruence 

pub fn montgomery_reduction_congruence() -> bool

Certify the Montgomery CONGRUENCE: (x + lo·q) − x = q·lo, so the reduction numerator differs from x by a multiple of q ⇒ redc·R ≡ x (mod q) ⇒ redc ≡ x·R⁻¹ (mod q) (R is a unit in 𝔽_q). A ring identity in the free variables x, lo, certified for all values.