proposition: Lemma size_ssub (s : form) (b : bool) : size (ssub (s,b)) <= 2 * f_size s.
proof: Proof. elim: s b => //= [|p|s IHs t IHt|s IHs|s IHs t IHt|s IHs t IHt] b; try by rewrite fsetU0 fset1Es. - apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _. apply: leq_ltn_trans (leq_add (IHs _) (IHt _)) _. apply/leP; rewrite -!(multE,plusE); lia. - apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (IHs _) _. apply/leP; rewrite -!(multE,plusE); lia. - apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU1 _ _) _. rewrite mulnS add2n !ltnS mulnDr. apply: leq_trans (fsizeU _ _) _. exact: leq_add. - apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU1 _ _) _. rewrite mulnS add2n !ltnS mulnDr. apply: leq_trans (fsizeU _ _) _. exact: leq_add. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) Lia