#m #n #a #b #ltam #ltbn #pnm
cut (andb (eqb ((cr_pair m n a b) \mod m) a)
(eqb ((cr_pair m n a b) \mod n) b) = true)
- [@f_min_true cases(congruent_ab_lt m n a b ?? pnm)
+ [whd in match (cr_pair m n a b) @f_min_true cases(congruent_ab_lt m n a b ?? pnm)
[#x * * #cxa #cxb #ltx @(ex_intro ?? x) % /2/
- >eq_to_eqb_true
+ >eq_to_eqb_true
[>eq_to_eqb_true // <(lt_to_eq_mod …ltbn) //
|<(lt_to_eq_mod …ltam) //
]