proposition: Lemma DH_prop2_from_bis: s 0 = 0 -> Dijkstra_prop2bis -> Dijkstra_prop2.
proof: Proof. move => sv0 hyp a b. pose prop2_aux a b := exists n m p, [/\ n + m = 2^p, a = s n & b = s m]. have sym u v: prop2_aux u v -> prop2_aux v u. by move => [n [m [k [ha hb hc]]]]; exists m, n, k; split => //; rewrite addnC. case:b; first by rewrite /coprime gcdn0 => /eqP ->; exists 1,0,0. move => b /hyp [k [ -> ->]]. case: (posnP k) => kp; first by rewrite kp DH_1 sv0; exists 0,1,0. case ek1: (k==1). by rewrite (eqP ek1) - (muln1 2) -[2]/(2^1) DH_power_two; exists 1,1,1. suff: forall m, ~~(odd m) -> prop2_aux (s m) (s m.+1). move => H; case ok: (odd k); last by apply: H => //; rewrite ok. move:(DH_palindrome_res kp); move => [m [hm -> ->]]. by apply: sym; apply: H; move: hm; rewrite oddD ek1 ok addbT. move => m om. case mz: (m ==0); first by rewrite (eqP mz); exists 0,1,0. exists (base2rev m.+1.-1), (bin_invert (base2rev m.+1)),(log2 m.+1); split. + by apply:base2_rev_invert => /=; rewrite ?om //eqSS mz. + by rewrite succnK DH_FR. + by rewrite DH_BI DH_FR. 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)