proposition: Lemma fusc_bezout_minimal n i (a := fusc (2 ^ n + i))(b:= fusc (2 ^ n + i.+1)): i < 2 ^n -> fusc i.+1 * a = fusc i * b + 1 /\ (forall u v, u* a = v * b +1 -> (fusc i.+1 <= u) && (fusc i <= v)).
proof: Proof. move => H. move: (fusc_bezout2 H); rewrite -/a -/b addnC mulnC (mulnC b) => eq1. have ha: fusc i < a by rewrite(ltn_leqif (fusc_bound (ltnW H))) (ltn_eqF H). split => // u v eq2. exact:(minimal_bezout_prop eq1 ha (fusc_bound H) eq2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)