proposition: Lemma DH_prop2_to_bis: s 0 = 0 -> Dijkstra_prop2 -> Dijkstra_prop2bis.
proof: Proof. move=> sv0 hyp a b. case eab:(a==b.+1). rewrite -(eqP eab) /coprime -{2} (mul1n a) gcdnMl => /eqP ->. by exists 1; rewrite (DH_power_two 1 1) DH_1. move: eab; case: a. by rewrite /coprime gcd0n => _ /eqP ->; exists 0; rewrite sv0 DH_1. move => a eab cp. have: a.+1 != 0 by []. have: b.+1 != 0 by []. move /hyp: cp => [n [m [p []]]]. case:m => [ |m nmp av bv]; first by rewrite sv0. move: eab nmp; rewrite av bv. case: (elogn2P m) => k q -> nsv nmp. move:(leq_addl n (2 ^ k * q.*2.+1)); rewrite nmp => le1. have pp:0 < 2^k by rewrite expn_gt0. have: 0 < q.*2.+1 by rewrite ltnS. rewrite -(leq_pmul2l pp) muln1 => eq3. move: (leq_trans eq3 le1); rewrite leq_exp2l // => lekp. move: nmp; rewrite -{1}(subnK lekp) (addnC _ k) expnD => nmp. move:(addnK (2 ^ k * q.*2.+1) n); rewrite nmp - mulnBr => eq4. move: nsv. rewrite - eq4 ! DH_power_two; set w := _ - _. have nmp': w + q.*2.+1 = 2 ^ (p - k). rewrite /w; apply: subnK. by rewrite -(leq_pmul2l pp) - nmp; apply: leq_addl. case: (posnP (p - k)) => ltkp. move /eqP:nmp'; rewrite ltkp /= addnS eqSS addn_eq0. by move => /andP [/eqP -> /eqP ->]; exists 0. case: (odd_dichot w) => ow2; last first. have: (odd (2 ^ (p - k))) by rewrite -nmp' oddD ow2 /= !odd_double /=. by rewrite oddX /= orbF => /eqP e0; move: ltkp; rewrite e0. move: nmp'; rewrite ow2 - (prednK ltkp). move:(w./2) ((p-k).-1). clear a b n m p k ltkp le1 pp eq3 lekp nmp eq4 w ow2 av bv. move => q' p. wlog: q q' / q' <= q. move => H eq1 neq1 anz bnz. case/orP:(leq_total q' q) => leqq; first by apply: H. rewrite addnC in eq1; rewrite eq_sym in neq1. move:(H q' q leqq eq1 neq1 bnz anz) => [k [eqa eqb]]. case: (posnP k) => kz; first by move: anz; rewrite eqa kz sv0. move:(DH_palindrome_res kz) => [m [_ ma mb]]. by exists m; rewrite eqa eqb ma mb. move => le1 nmp nsv _ _ ; move: le1. rewrite leq_eqVlt; case/orP => le1. by move/eqP: nsv; rewrite (eqP le1). have le2: q'.*2.+1 < q.*2.+1 by rewrite ltnS ltn_double. have ok: odd (q.*2.+1) by rewrite /= odd_double. set w := q'.*2.+1. have /andP[ le3 le4]: w <2^p <= q.*2.+1. rewrite -(leq_add2l w (2^p) q.*2.+1); move: (ltn_add2l w w q.*2.+1). rewrite nmp /w le2 expn2S addnn ltn_double - (addnn (2^p)) leq_add2r=> h. by rewrite h /= (ltnW h). have ln: log2 (q.*2.+1) = p.+1. apply: log2_pr;rewrite le4 /=; case:(posnP w) => wp. by move: ok;rewrite - (add0n q.*2.+1) - wp nmp expn2S odd_double. by rewrite - nmp -/w - (prednK wp) addSn ltnS leq_addl. have oiq:= (bin_invert_odd ok). set n := base2rev(bin_invert (q.*2.+1)). have eq3: bin_invert (base2rev n) = q.*2.+1. by rewrite /n (base2rev_oddI oiq) bin_invertI. case: (posnP (bin_invert q.*2.+1)) => sa; first by move: oiq; rewrite sa /=. case: (posnP n) => nz; first by move:eq3; rewrite nz //. have on : odd n by rewrite /n - (prednK sa); apply: odd_base2rev. rewrite /w - eq3 DH_BI DH_FR. case en1:(n==1). move: eq3; rewrite (eqP en1) /bin_invert/base2rev /= => eq4. by move: le2; rewrite - eq4 ltnS ltn0. move: (log_base2r oiq) nmp; rewrite log2_bin_invert -/n ln => <-. move/eqP;rewrite - eq3 - (base2_rev_invert on (negbT en1)) eqn_add2r => /eqP ->. by rewrite DH_FR -{2}(prednK nz); exists (n.-1). 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)