proposition: Lemma ins_ins k1 k2 v1 v2 (s : fmap) : ins k1 v1 (ins k2 v2 s) = if k1 == k2 then ins k1 v1 s else ins k2 v2 (ins k1 v1 s).
proof: Proof. rewrite /ins; case: s => s H; case H1: (k1 == k2); rewrite fmapE /=. - rewrite (eqP H1) {H1}. elim: s H k2 v1 v2=>[|[k3 v3] s IH] /= H k2 v1 v2; first by rewrite irr eq_refl. case: (totalP k2 k3)=>H1 /=; rewrite ?irr ?eq_refl //. case: (totalP k2 k3) H1=>H2 _ //. by rewrite IH //; apply: path_sorted H. elim: s H k1 k2 H1 v1 v2=>[|[k3 v3] s IH] H k1 k2 H1 v1 v2 /=. - rewrite H1 eq_sym H1. by case: (totalP k1 k2) H1=>H2 H1. case: (totalP k2 k3)=>H2 /=. - case: (totalP k1 k2) (H1)=>H3 _ //=; last first. - by case: (totalP k1 k3)=>//= H4; rewrite ?H2 ?H3. case: (totalP k1 k3)=>H4 /=. - case: (totalP k2 k1) H3=>//= H3. by case: (totalP k2 k3) H2=>//=. - rewrite (eqP H4) in H3. by case: (totalP k2 k3) H2 H3. by case: (totalP k1 k3) (trans H3 H2) H4. - rewrite -(eqP H2) {H2} (H1). case: (totalP k1 k2) (H1)=>//= H2 _; rewrite ?irr ?eq_refl //. rewrite eq_sym H1. by case: (totalP k2 k1) H1 H2. case: (totalP k1 k3)=>H3 /=. - rewrite eq_sym H1. case: (totalP k2 k1) H1 (trans H3 H2)=>//. by case: (totalP k2 k3) H2=>//=. - rewrite (eqP H3). by case: (totalP k2 k3) H2. case: (totalP k2 k3)=>H4 /=. - by move: (trans H4 H2); rewrite irr. - by rewrite (eqP H4) irr in H2. by rewrite IH //; apply: path_sorted H. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq path) LemmaOverloading(ordtype prelude)