proposition: Lemma nds_add_sb_inj x y u v: ordinalp x -> ordinalp y -> nds_binomp u -> nds_binomp v -> (nds_shift x) +o u = (nds_shift y) +o v -> x = y /\ u = v.
proof: Proof. move => ox oy bu bv eq. set a := oopow \2o *o x +o u; set b := oopow \2o *o y +o v. set c := oopow \2o. have ou:= proj31_1 bu. have ov:= proj31_1 bv. have oc := OS_oopow OS2. have oa := OS_sum2 (OS_prod2 oc ox) ou. have ra: odiv_pr0 a c x u by split. have rb: odiv_pr0 a c y v by rewrite /a -/(nds_shift _) eq; split => //. exact: (odivision_unique oa oc ra rb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)