proposition: Lemma fweight_neq_0 : (forall f, fweight f <> 0) /\ forall l, lweight l <> 0.
proof: Proof. assert (fe:=fun_elim (f:=fweight)). apply prod_conj. apply (fe (fun l n => n <> 0) (fun l n => n <> 0)); intros; lia. Qed.
imports: Equations(Equations) Lia