proposition: Lemma DH_prop1_to_bis: Dijkstra_prop1 -> Dijkstra_prop1bis.
proof: Proof. move => hyp n. wlog: n/ ~~(odd n). move => H; case on: (odd n); last by apply: H => //; rewrite on. case: (posnP n) => nz;first by rewrite nz DH_1 /coprime gcdn1. case n1: (n==1); first by rewrite (eqP n1) DH_1 coprime1n. move:(DH_palindrome_res nz) => [m [mp -> ->]]. rewrite /coprime gcdnC;apply: H. by move: mp; rewrite n1 oddD on /= addbT. case: n=> [ | n on ]; first by rewrite DH_1 coprimen1. move: (base2_rev_invert (on: odd n.+2) (is_true_true: (n.+2 != 1))). by move/hyp;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)